Termination Proof Script

Consider the TRS R consisting of the rewrite rule


1:		app(app(:,app(app(:,app(app(:,app(app(:,C),x)),y)),z)),u)	→ app(app(:,app(app(:,x),z)),app(app(:,app(app(:,app(app(:,x),y)),z)),u))

There are 9 dependency pairs:


2:		APP(app(:,app(app(:,app(app(:,app(app(:,C),x)),y)),z)),u)	→ APP(app(:,app(app(:,x),z)),app(app(:,app(app(:,app(app(:,x),y)),z)),u))
3:		APP(app(:,app(app(:,app(app(:,app(app(:,C),x)),y)),z)),u)	→ APP(:,app(app(:,x),z))
4:		APP(app(:,app(app(:,app(app(:,app(app(:,C),x)),y)),z)),u)	→ APP(app(:,x),z)
5:		APP(app(:,app(app(:,app(app(:,app(app(:,C),x)),y)),z)),u)	→ APP(app(:,app(app(:,app(app(:,x),y)),z)),u)
6:		APP(app(:,app(app(:,app(app(:,app(app(:,C),x)),y)),z)),u)	→ APP(:,app(app(:,app(app(:,x),y)),z))
7:		APP(app(:,app(app(:,app(app(:,app(app(:,C),x)),y)),z)),u)	→ APP(app(:,app(app(:,x),y)),z)
8:		APP(app(:,app(app(:,app(app(:,app(app(:,C),x)),y)),z)),u)	→ APP(:,app(app(:,x),y))
9:		APP(app(:,app(app(:,app(app(:,app(app(:,C),x)),y)),z)),u)	→ APP(app(:,x),y)
10:		APP(app(:,app(app(:,app(app(:,app(app(:,C),x)),y)),z)),u)	→ APP(:,x)

The approximated dependency graph contains one SCC: {2,4,5,7,9}.

Consider the SCC {2,4,5,7,9}. By taking the AF π with π(APP) = 1 together with the lexicographic path order with empty precedence, the rules in {1,2,4,5,7,9} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (1.36 seconds) --- May 4, 2006